\chapter{\K Framework short overview}
\label{over}
In 2003, Grigore Ro\c{s}u, Assistant Professor at University of Illinois at Urbana-Champaign, introduced \K \cite{firstk} as a technique in his programming languages course. \K technique assumed to write what is today a \K definition and then translate it into Maude \cite{maude} by hand in order to execute it. Later, this process has been automated and now there is a prototype of \K  called K-Maude, which uses Maude Rewriting Engine as a backend.
As described in \cite{jlap2010}, \K is an executable semantic framework in which programming languages, calculi, as well as type systems or formal analysis tools can be defined, making use of {\it configurations}, {\it computations} and {\it rules}.\\
\K is inspired from rewriting logic but specialized and optimized for programming languages. It consists of three components: a concurrent rewrite abstract machine, a language definitional technique, and a specialized notation. The  rewrite abstract machine allows rules to overlap when they do not change the overlapped sub-term. This increases the potential of concurrency of a rewrite theory. Regarding \K as a language definitional technique we can say that it is based on intuitions from the chemical abstract machine (CHAM) \cite{cham}, evaluation contexts \cite{contexts}, and continuations \cite{continuations}.\\
In \K definitions a {\it configuration} is represented by a {\it nested cell} structure. {\it Configurations} organize the system/program state in units called {\it cells}, which are labeled and can be nested. {\it Computations} carry computational meaning as special nested list structures sequentializing computational tasks, such as fragments of program; in particular, computations extend the original language or calculus syntax. \K (rewrite) {\it rules} generalize conventional rewrite rules by making explicit which parts of the term they read, write, or do not care about.\\

To exemplify the \K Framework we will use here parts of the \K definition of SIMPLE, which is completely defined in Appendix (chapter \ref{appendix}).


\section{SIMPLE}
\label{over:simple}



SIMPLE \cite{kpage} is intended to be a pedagogical language that captures the essence of the imperative programming paradigm, extended with several features often encountered in imperative programming languages. A program consists of a set of global variable declarations and function definitions.  Like in C, function definitions cannot be nested and each program must have one function called \texttt{main}, which is invoked when the program is executed. To make it more interesting and to highlight some of \K's strengths, SIMPLE includes the following features in addition to the conventional imperative expression and statement constructs:

\begin{itemize}
\item Multidimensional arrays and array references.  An array evaluates to an array reference, which is a special value holding a location where the elements of the array start together with the size of the array; the elements of the array can be array references themselves when the array is multi-dimensional.  Array references are ordinary values, so they can be assigned to variables and passed/received by functions.

\item Functions and function references.  Functions can have zero or more parameters and can return abruptly using a \texttt{return} statement. SIMPLE is call-by-value with static scoping.  Function names evaluate to function references, which hereby become ordinary values in the language, same like the array references.

\item Blocks with locals.  SIMPLE allows variables to be declared anywhere, their scope being the most nested block containing them.
 
\item Input/Output.  The expression \texttt{read()} evaluates to the next value in the input buffer, and the statement \texttt{write(e)}
 evaluates \texttt{e} and outputs its value to the output buffer.  The
 input and output buffers are lists of values.
\item Exceptions.  SIMPLE has parametric exceptions (the value thrown as an exception can be caught and bound).

\item Concurrency via dynamic thread creation/termination and synchronization.  One can spawn a thread to execute any statement. The spawned thread shares with its parent its environment at creation time. Threads can be synchronized via reentrant locks which can be acquired and released, as well as through rendezvous.

\end{itemize}

In order to give the user a better understanding of \K  we present here some parts of the definition of SIMPLE language: statements syntax, configuration and variable look-up rule. 

\begin{figure}[h]
\centering
\begin{minipage}{.6\textwidth}
 \syntax{\nonTerminal{\sort{Stmt}}}{\terminal{\{}{\nonTerminal{\sort{Stmts}}}\terminal{\}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{\{\}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{{\nonTerminal{\sort{Exp}}}\terminal{;}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{if}{\nonTerminal{\sort{Exp}}}\terminal{then}{\nonTerminal{\sort{Stmt}}}\terminal{else}{\nonTerminal{\sort{Stmt}}}}{\kstrict{1}{}}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{if}{\nonTerminal{\sort{Exp}}}\terminal{then}{\nonTerminal{\sort{Stmt}}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{while}{\nonTerminal{\sort{Exp}}}\terminal{do}{\nonTerminal{\sort{Stmt}}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{for}{\nonTerminal{\sort{Id}}}\terminal{=}{\nonTerminal{\sort{Exp}}}\terminal{to}{\nonTerminal{\sort{Exp}}}\terminal{do}{\nonTerminal{\sort{Stmt}}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{return}{\nonTerminal{\sort{Exp}}}\terminal{;}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{write(}{\nonTerminal{\sort{Exp}}}\terminal{);}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{try}{\nonTerminal{\sort{Stmt}}}\terminal{catch(}{\nonTerminal{\sort{Id}}}\terminal{)}{\nonTerminal{\sort{Stmt}}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{throw}{\nonTerminal{\sort{Exp}}}\terminal{;}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{spawn}{\nonTerminal{\sort{Stmt}}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{acquire}{\nonTerminal{\sort{Exp}}}\terminal{;}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{release}{\nonTerminal{\sort{Exp}}}\terminal{;}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{rendezvous}{\nonTerminal{\sort{Exp}}}\terminal{;}}{\kstrict{}{}}
 \syntax{\nonTerminal{\sort{Stmts}}}{{\nonTerminal{\sort{Stmts}}}\mathrel{}{\nonTerminal{\sort{Stmts}}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmts}}}{\crlbracket{\nonTerminal{\sort{Decl}}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmts}}}{\crlbracket{\nonTerminal{\sort{Stmt}}}}{}
\end{minipage}\\
\label{stmts}
\caption{SIMPLE: statements syntax}
\end{figure}



The syntax of statements of SIMPLE language is shown in Figure \ref{stmts}. Most of the statement constructs are standard for imperative languages. We also syntactically distinguish between empty and non-empty blocks. Variables can be declared anywhere inside a block, their scope ending with the block. Expressions are allowed to be used for their side-effects only (followed by a semicolon ``\texttt{;}''). Functions are allowed to abruptly return. The exceptions are parametric, i.e., one can throw a value which is bound to the variable declared by \texttt{catch}. Threads can be dynamically created and terminated, and can synchronize with \texttt{acquire}, \texttt{release} and \texttt{rendezvous}. Note that the strictness attributes obey the intended evaluation strategy of the various constructs.  In particular, the if-then-else construct is strict only in its first argument (the if-then construct will be desugared into if-then-else), while the loops constructs are not strict in any arguments. 


The \K configuration (Figure \ref{config:S}) of SIMPLE consists of a top level cell, \textsf{T}, holding a \textsf{threads} cell, a global environment map cell \textsf{genv} mapping the global variables and function names to their locations, a shared store map cell \textsf{store} mapping each location to some value, a set cell \textsf{busy} holding the locks which have been acquired but not yet released by threads, \textsf{input} and \textsf{output} list cells, and a \textsf{nextLoc} cell holding a natural number indicating the next available location.  



For simplicity, the location counter in \textsf{nextLoc} models an actual physical location in the store (and assumes no garbage collection).  The \textsf{threads} cell contains one \textsf{thread} cell for each existing thread in the program.  Note that the thread cell has multiplicity ``*'', which means that at any given moment there could be zero, one or more \textsf{thread} cells.  Each \textsf{thread} cell contains a computation cell \textsf{k}, a \textsf{control} cell holding the various control structures needed to jump to certain points of interest in the program execution, a local environment map cell \textsf{env} mapping the thread local variables to locations in the store, and finally a \textsf{holds} map cell indicating what locks have been acquired by the thread and not released so far and how many times (SIMPLE's locks are re-entrant). The \textsf{control} cell currently contains only two subcells, a function stack \textsf{fstack} which is a list and an exception stack \textsf{xstack} which is also a list.  One can add more control structures in the \textsf{control} cell, such as a stack for break/continue of loops, etc., if the language is extended with more control-changing constructs.  Note that all cells except for \textsf{k} are also initialized, in that they contain a ground term of their corresponding sort.  The \textsf{k} cell needs not be initialized at this level, because it will be initialized with the program to evaluate later. 

In Figure \ref{look} the variable look-up rule is shown using the \K graphical notation as for configuration (Figure \ref{config:S}).


When a variable $X$ is the first computational task (note the rupture of the \textsf{k} cell to the right), and $X$ is bound to some location $L$ in the environment (note the rupture of the \textsf{env} cell at both sides), and $L$ is mapped to some value $V$ in the store, then rewrite $X$ by $V$. All the other \K rules from SIMPLE definition are written in the same way, by specifying the cells which are relevant for the current rewrite. 

The full semantics of SIMPLE can be found in the Appendix. 